FAQ #2 по Groupoid Infinity 1. Я слышал, что верификация критоповлют и их языков достаточно сложная тема. Ведь чтобы верифицировать язык и его модель — это уже нужно полностью ее загнать в Coq/Agda, а нужно ведь еще верифицировать компилятор или виртуальную машину, что она сохраняет свои свойства. Как вы это все собираетесь писать двумя человеками? Если идти таким путем, который описан в вопросе, то может выглядеть действительно сложно. Однако мы сторонники PCC подхода, где теоремы (свойства) поставляются в том же языке на котором написан исполняющийся код. В нашем случае — это OM. Другой пример такой платформы как идеи распространения trusted кода по Internet — это Morte. В ACL2 (прувер для инженеров) тоже код экстрактился в Common Lisp вместе с проверками свойств. Наш подход немножко другой чем предоставление Сертифицированной Виртуальной Машины, Языка Контрактов и его Сертифицированного Компилятора. Вместо этого мы предлагаем писать на DSL с зависимыми типами (кванторами) а виртуальной машиной будет служить виртуальная машина Erlang, достаточно надежная если работать в ней без эффектов. Код лямбда ядра OM будет превращаться в код исполнительной среды. Терминированность обеспечивается самим тайчекером и теоремами которые поставляются вместе с кодом и чекаются на стороне сервера. Этот подход подразумевает распространение микропограмм на чистой лямбде в качестве трастед виратуальной машины (никто ведь не будет спорить что лямбда кор более трастед чем любая штука, которую могут придумать люди, добавив свою extra complexity для решения теоретических сложностей или технический сложнойстей (производительности). ОМ и есть трастед виртуальная машина, имплементацию которой подменяет subset Erlang, который может только лямбды апплицировать. Верифицировать такую машину проще, чем кастомные машины для контрактов. Но мы не только не разрабатываем виртуальную машину, мы также не особо разрабатываем язык контрактов. Для нас это разработка языка с зависимыми типами EXE с компактной библиотекой в духе Elm, а прикладные задачи (пакетные фильтры, бизнес контракты) — это просто DSL на этом языке. Все эти прикладные задачи описывают алгоритмы которые экстрактятся в lambda core, инкрустированные универсальными квантификаторами. 2. Я слышал что в любых системах нужно писать Unit тесты. Даже когда вы доказываете свойства систем. Может ваша система доказать мой код на Scala/C# ? Ну давайте посмотрим как повышают качество ПО: — Unit tests — TDD/BDD — Property testing — Formal Methods Мы работаем в контексте последнего пункта — формальных методов. Наш продукт не является системой похожей на QuickCheck ни более того никак не связан с тестированием фунционального и семантического наполнения ваших моделей. Т.е. мы пока не строим модели на заказ (пока не было заказов), а разрабатываем инфраструктурные элементы системы исполнения и редистрибюции верифицированного кода, который проходит тайпчек — как если бы это были сертификаты, которые совпадают с наперед сформулированными теоремами свойствами. В этих свойствах вы можете например лимитировать время тайпчека или размеры выделяемой памяти в процессе его работы. Но для этого нужно использовать язык с кванторами. Т.е. пока вы не используете кванторы — вы просто занимаетесь композицией аксиом MLTT. При этом вы можете продолжать оставаться в System Fw, но как только вы захотите доказать какое-то свойство ваших конструкций, вам придется выйти в зависимую теорию, и ваш код при этом будет похож на Coq/Agda/Lean. Т.е. без кванторов — это должен быть обычный язык уровня ML или начальных Haskell-ов — с минимумом конструкций, только с record (они же модули) и data. Паттерн мачинг понятный эрланг программисту и дюжиной примитивов в базовой библиотеке для построение систем, которые обычно строят на платформе Erlang/OTP. 3. Почему ядро без Sigma, Equ, Fix/Rec? Мы можем также взять переписать тайпчекер Lean из Хаскеля на эрланг и получить новый байткод и новое лямбда ядро, совместимое например с Lean, но мне показалось, что чем проще ядро — тем более к нему доверия можно вызвать у индустрии. OM реально доступен любому инженеру для понимания. Сложные пруверы с большим ядром требуют объяснения. Возможно будут и другие ядра, но пока идея с OM ядром очень интересна, так как в ней возможно вычисление лимитов начальных алгебр, а значит вы можете использовать индуктивные типы и весь инструментарий на котором сформулированы все современные теоремы. Наш язык не будет включать никаких тактик или чего-то похожего, так как это ведет к развувания ядра, а ощутимой пользы не приносит, приходится руками заниматься композициями высказываний в другом DSL. Зачем? Если можно было просто заниматься композицией высказываний в том же хост-языке и держать теоремы в носителях типов и значений, в рекордах. Такой рекорд с функциональностью и теоремами называется PCC и может редистрибуцироваться по ненадежным каналам. Idris например тоже изначально содержал язык тактик для интерактивного доказательства теорем, но потом его разработка была приоставлена, так как усложнялось ядро прувера. 4. Зачем мне еще один Coq? Дело в том, что Coq — это язык для математиков, EXE — это язык для инженеров которые работают с буферами грубо-говоря. Нас интересуют пока только алгоритмы связанные со стримами или бесконечными/конечными списками и их процессиногом в условиях распределенной работы. И нас интересует максимально простая форма ПиСигма языка, которая была сравнима с тем, как Эрланг проще всех остальных языков. Если этот язык и его базовая библиотека окажется слишком сложным в использовании (Например сложнее чем Хаскель или Scala), то мы будем считать, что наша задача не выполнена. 5. Одна из проблем существующих пруверов, как мне объяснили и как я понял - интерактивность. То есть они все требуют каких-то отношений с живым человеком, чтобы правильно все проверить. Будет ли у вас так же или будет возможность в одну трубу закинуть код, в другую какие-то параметры, и получить ответ на выходе? Мы не продаем никакой интерактивности. Конечно у нас будет pretty print colored eval (just like in Elixir, потому что мы по сути просто еще один Erlang язык), но так как в языке нет тактик для рабочего матемаика, то это скорее язык для инженеров. А инженеров не заставишь писать алгоритмы в графических редакторах (именно поэтому пока в BPE отсувствует векторный редактор Workflow). Никакой магии наш прувер не предоставляет, это все лишь (в порядке увеличения крутости поставленных целей): — просто нормальный Хаскель для Erlang — ядро прувера — top-level язык Erlang с родным экстрактом и биндингами (маршалингом) типов Erlang — библиотека теорем для хранения цепочек — библиотеки для распределенного алгоритма чейн репликация — криптовалюты, блокчейн и т.д. 6. Есть ли какой-то способ с помощью OM/EXE верифицировать не только код, на нем написанный, но и код на других языках? Есть стандартный подход для верификации программ на других языках. Строится модель языка на котором написан код, строится транформация конкретной программы из этой модели в рабочую метатеорию, доказывается изоморфизм этого построения, доказываются свойства преобразованной программы в метатеории. В зависимости от класса программ метатоерии в которых будут работать математики доказывая ваш код могут отличаться. Как правило сейчас на рынке все хотят верифицировать С код. Мы не соревнуемся на этом рынке никоим образом, и наш подход полностью исключает такую модель построения доказательств. Если вы хотите ферифицировать C код, вам нужно взять VST CompCert С компилятор, написанный на Coq, преобразовывать С программы в Coq листинги и работать уже продолжать в Coq. Мы считает такой подход полным фейлом, та как это требует отдела R&D для выполнения это работы. Вы конечно можете нанять консультантов, ребята из http://www.functor.se вам все сделают за дорого, там лично у них советник Альтенкирх http://www.functor.se/company/leadership/ Мы поставщики совершенно другого подхода. Мы предлагаем тоже платформу но в которой доказательства строятся не через доказательство изоморфных экземпляров теорий, а вытаскивается в target язык напрямую из описание программы написанной на EXE, который мы хотим сделать engineer friendly. В идеальном случае, предствате, что все типы в нашей базовой библиотеке поставляются с основными теоремами и вы просто пишете какой-то сетевой код или сервисы для стриминг процессинга используя этот Haskell для Erlang, как обычный программист, не задумывясь особо о построении метамодели. Потом математик просто проставляет PCC, или мы наперед пишем программы исходя из заданных PCC. Важно тут что для программиста — это должно выглядеть как еще один Elixir с кванторами и странным синтаксисом или Elm с бекендом в Erlang вместо JavaScript.